A, B:Realizer. R-Feasible(A)  R-Feasible(B)  A || B  interface-compatible([[A]];[[B]]) 

latex

Definitions

x:A. B(x), t  T, P  Q, AB, A, False, ij, SQType(T), {T}, Prop, A & B, R-size(R), R-Feasible(R), [[R]], x. t(x), P & Q, x:A. B(x), if b t else f fi, true, P  Q, P  Q, false, T, True, , , Dec(P), P  Q, Realizer, Unit, x(s), A || B, Y, Rplus?(x1), Rplus-left(x1), Rplus-right(x1), Rnone?(x1), , , , left  right, @loc x initially v:T, @loc only events in L change x:T, only events in L send on lnk with tag, @loc effect knd(v:T)  x := f State(ds) v , sends knd(v:T) on l:tagged(g,State(ds),v):dt, @loc precondition for a(v:T):P State(ds) v, @loc: k writes only members of L, @loc: k sends only on links in L, @loc: only members of L read x, S  T

Lemmas

nat wf, nat properties, ge wf, R-size wf, le wf, nat plus wf, es realizer wf, decidable int equal, R-Dsys wf, R-interface-base, R-size-decreases, Rplus-right wf, Rplus-left wf, assert wf, Rplus? wf, R-compat wf, R-Feasible wf, decidable le, unit wf, Id wf, Knd wf, IdLnk wf, fpf wf, decl-state wf, decl-type wf, not wf, Rnone wf, true wf, Rplus wf, Rinit wf, atom-free wf, Rframe wf, normal-type wf, Rsframe wf, Reffect wf, normal-ds wf, isrcv wf, ldst wf, lnk wf, Rsends wf, eq lnk wf, fpf-cap wf, id-deq wf, tagof wf, lsrc wf, Rpre wf, decidable wf, Raframe wf, Rbframe wf, Rrframe wf, interface-compatible-join, R-compat-implies, R-compat-Rplus2, interface-compatible-join2, R-compat-symmetry, ifthenelse wf, le int wf, nat plus inc, bool wf, iff transitivity, eqtt to assert, assert of le int, lt int wf, bnot wf, eqff to assert, squash wf, bnot of le int, assert of lt int